Nuprl Lemma : frame-compatible-R-base-ma-pair
11,40
postcript
pdf
A
,
B
:Realizer.
R-Feasible(
A
)
R-frame-compat(
A
;
B
)
ma-frame-compat(R-base-ma(
A
);R-base-ma(
B
))
latex
Definitions
P
Q
,
A
,
A
B
,
False
,
t
T
,
x
.
t
(
x
)
,
{
i
..
j
}
,
i
j
<
k
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
x
(
s
)
Lemmas
pi2
wf
,
decl-state
wf
,
select
wf
,
lnk-decl-cap
,
subtype
rel
self
,
fpf-cap
wf
,
Id
wf
,
id-deq
wf
origin
A, B:Realizer.
R-frame-compat(A;B) ma-frame-compat(R-base-ma(A);R-base-ma(B)) A, B:Realizer.
R-frame-compat(A;B) ma-frame-compat(R-base-ma(A);R-base-ma(B)) Q
A
B
T
x. t(x)
} j < kx:A. B(x)